-
Notifications
You must be signed in to change notification settings - Fork 353
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Issue discovered in TB: spurious reads are not (yet) possible in a concurrent setting #3054
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Vanille-N
force-pushed
the
spurious-fail
branch
2 times, most recently
from
September 7, 2023 20:18
f9b83a0
to
ca60656
Compare
RalfJung
reviewed
Sep 11, 2023
RalfJung
reviewed
Sep 12, 2023
RalfJung
reviewed
Sep 12, 2023
RalfJung
reviewed
Sep 12, 2023
RalfJung
reviewed
Sep 12, 2023
RalfJung
reviewed
Sep 12, 2023
RalfJung
reviewed
Sep 14, 2023
RalfJung
reviewed
Sep 14, 2023
RalfJung
reviewed
Sep 14, 2023
RalfJung
reviewed
Sep 14, 2023
RalfJung
reviewed
Sep 14, 2023
RalfJung
reviewed
Sep 14, 2023
RalfJung
reviewed
Sep 14, 2023
RalfJung
reviewed
Sep 19, 2023
RalfJung
reviewed
Sep 19, 2023
RalfJung
reviewed
Sep 19, 2023
RalfJung
reviewed
Sep 19, 2023
Just one last comment nit. :) Then please squash the commits and we're good to go. |
r=me after squashing and fixing that comment. |
✌️ @Vanille-N, you can now approve this pull request! If @RalfJung told you to " |
This occurs because in some interleavings, inserting a spurious read turns a Reserved into Frozen. We show here an exhaustive test (including arbitrary unknown code in two different threads) that makes this issue observable.
Vanille-N
force-pushed
the
spurious-fail
branch
from
September 19, 2023 15:33
2437842
to
69272a8
Compare
☀️ Test successful - checks-actions |
bors
added a commit
that referenced
this pull request
Oct 6, 2023
Continuation of #3054: enable spurious reads in TB The last additions to the test suite of TB left some unresolved `#[should_panic]` that these new modifications solve. ## Problem Recall that the issues were arising from the interleavings that follow. ### A. `Reserved -> Frozen` has visible effects after function exit The transition `Reserved -> Frozen` irreversibly blocks write accesses to the tag, so in the interleaving below `y` initially `Reserved` becomes `Frozen` only in the target where a spurious read through `x` is inserted. This makes the later write through `y` UB only in the target and not in the source. ``` 1: retag x (&, protect) 2: retag y (&mut, protect) 1: spurious read x 1: ret x 2: ret y 2: write y ``` ### B. Protectors only announce their presence on retag There is a read-on-reborrow for protected locations, but if the retag of `x` occurs before that of `y` and there is no explicit access through `x`, then `y` is unaware of the existence of `x`. This is problematic because a spurious read inserted through `x` between the retag of `y` and the return of the function protecting `x` is a noalias violation in the target without UB in the source. ``` 1: retag x (&, protect) 2: retag y (&mut, protect) 1: spurious read x 1: ret x 2: write y 2: ret y ``` ## Step 1: Finer behavior for `Reserved` Since one problem is that `Reserved -> Frozen` has consequences beyond function exit, we decide to remove this transition entirely. To replace it we introduce a new subtype of `Reserved` with the extra boolean `aliased` set. `Reserved { aliased: true }` forbids child accesses, but only temporarily: it has no effect on activation once the tag is no longer protected. This makes the semantics of Tree Borrows slightly weaker in favor of being more similar to noalias. This solves interleaving **A.**, but **B.** is still a problem and the exhaustive tests do not pass yet. ## Step 2: Read on function exit Protected tags issue a "reminder" that they are protected until this instant inclusive, in the form of an implicit read (symmetrically to the implicit read on retag). This ensures that if the periods on which two tags `x` and `y` are protected overlap then no matter the interleaving of retags and returns, there is either a protector currently active or a read that has been emitted, both of which temporarily block activation. This makes the exhaustive test designed previously pass, but it has an effect on the ability to return an activated pointer that I had not foreseen before implementing it. ## Step 2': Do not propagate to children A naive implementation of **Step 2** makes the following code UB: ```rs fn reborrow(x: &mut u8) -> &mut u8 { let y = &mut *x; *y = *y; y // callee returns `y: Active`... } let x = &mut 0u8; let y = reborrow(x); // ... and caller receives `y: Frozen` *y = 1; // UB ``` This is unacceptable, and a simple fix is to make this implicit read visible only to foreign tags. We still lack hindsight on the ramifications of this decision, and the fact that the problematic pattern was only discovered because it occured in one completely unrelated test (with a cryptic error message) is worrying. We should be vigilant as to how this interacts with the rest of the model. ## TODO As of commit #281c30, the data race model has not been fully updated. We have removed the reborrow of mutable references counting as a write access, but we still need the implicit read of function exit to count as a read.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We discovered a week ago that in general, the current model of TB does not allow spurious reads because although reads provably never invalidate other reads, they migh invalidate writes.
Consider the code
of which one possible interleaving is
that does not have UB.
Assume enough barriers to force this specific interleaving, and consider that the compiler could choose to insert a spurious read throug
x
during the call tof1
which would produceThus the target of the optimization (with a spurious read) has UB when the source did not.
This is bad.
SB is not affected because the code would be UB as early as
retag y
, this happens because we're trying to be a bit more subtle than that, and because the effects of a foreign read on a protected&mut
bleed outside of the boundaries of the protector. Fortunately we have a fix planned, but in the meantime here are some#[should_panic]
exhaustive tests to illustrate the issue.The error message printed by the
#[should_panic]
tests flags the present issue in slightly more general terms: it says that the sequenceretag x (&, protect); retag y (&mut, protect);
produces the configurationC_source := x: [P]Frozen, x: [P]Reserved
, and that inserting a spurious read throughx
turns it intoC_target := x: [P]Frozen, y: [P]Reserved
.It then says that
C_source
is distinguishable fromC_target
, which means that there exists a sequence of instructions applied to both that triggers UB inC_target
but not inC_source
.It happens that one such sequence is
1: return f1; 2: return f2; 2: write y;
as shown above, but it is not the only one, as for example the interleaving1: return f1; 2: write y;
is also problematic.